package bcontractor.partialmeet;

import static org.hamcrest.Matchers.equalTo;
import static org.hamcrest.Matchers.is;
import static org.junit.Assert.assertThat;

import org.junit.Before;
import org.junit.Test;

import bcontractor.api.RevisionOperator;
import bcontractor.api.SATReasoner;
import bcontractor.api.SentenceSet;
import bcontractor.base.SetUtils;
import bcontractor.propositional.MiniSatReasonerBuilder;
import bcontractor.propositional.PropositionalSentence;
import bcontractor.propositional.SentenceParser;

/**
 * Unit test for partial meet revision operator using full selection function.
 * 
 * @author lundberg
 * 
 */
public class FullPartialMeetRevisionOperatorShould {

    private RevisionOperator<PropositionalSentence> revision;

    private SATReasoner<PropositionalSentence> reasoner;

    private SentenceParser parser;

    @Before
    public void init() {
        this.revision = PartialMeetRevisionOperatorBuilder.aRevisionOperator().build();
        this.reasoner = MiniSatReasonerBuilder.aReasoner().build();
        this.parser = new SentenceParser();
    }

    @Test
    public void stripSentenceStraightforward() {
        SentenceSet<PropositionalSentence> base = this.parser.createSet("a", "b", "a v b");
        PropositionalSentence target = this.parser.create("¬a");
        SentenceSet<PropositionalSentence> result = this.revision.eval(base, target);
        assertThat(this.reasoner.isSatisfiable(result), is(true));
        assertThat(this.reasoner.entails(result, target), is(true));
        assertThat(result, equalTo(this.parser.createSet("¬a", "b", "a v b")));
    }

    @Test
    public void stripSentencesThatEntailed() {
        SentenceSet<PropositionalSentence> base = this.parser.createSet("¬a v b", "a", "c");
        PropositionalSentence target = this.parser.create("¬b");
        SentenceSet<PropositionalSentence> result = this.revision.eval(base, target);
        assertThat(this.reasoner.isSatisfiable(result), is(true));
        assertThat(this.reasoner.entails(result, target), is(true));
        assertThat(result, equalTo(this.parser.createSet("¬b", "c")));
    }

    @Test
    public void stripSentencesFromAllKernels() {
        SentenceSet<PropositionalSentence> base = SetUtils.emptySentenceSet();
        base = base.with(this.parser.createList("¬b v a", "b"));
        base = base.with(this.parser.createList("¬b v a", "¬c v ¬d v b", "¬e v d", "c", "e"));
        base = base.with(this.parser.createList("j v k", "m v n v ¬q", "m v ¬n v q v j"));

        PropositionalSentence target = this.parser.create("¬a");

        SentenceSet<PropositionalSentence> result = this.revision.eval(base, target);
        assertThat(this.reasoner.isSatisfiable(result), is(true));
        assertThat(this.reasoner.entails(result, target), is(true));

        assertThat(result, equalTo(this.parser.createSet("j v k", "m v n v ¬q", "m v ¬n v q v j", "¬a")));
    }

    @Test
    public void doNothingIfNotNecessary() {
        SentenceSet<PropositionalSentence> base = SetUtils.emptySentenceSet();
        base = base.with(this.parser.createList("¬b v a"));
        base = base.with(this.parser.createList("¬b v a", "¬c v ¬d v b", "¬e v d", "e"));
        base = base.with(this.parser.createList("j v k", "m v n v ¬q", "m v ¬n v q v j"));

        PropositionalSentence target = this.parser.create("¬a");

        SentenceSet<PropositionalSentence> result = this.revision.eval(base, target);

        assertThat(this.reasoner.isSatisfiable(result), is(true));
        assertThat(this.reasoner.entails(result, target), is(true));

        assertThat(result, equalTo(base.with(target)));
    }
}
